$\forall$$T$:Type, ${\it as}$:$T$ List, $R$:($T$$\rightarrow$$T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. $\neg$$R$($x$,$x$)) $\Rightarrow$ l{-}ordered($T$;$x$,$y$.$R$($x$,$y$);${\it as}$) $\Rightarrow$ no\_repeats($T$;${\it as}$)